Developers of performance-critical multi-threaded software often try to avoid the overhead of traditional locking. Traditional techniques for doing so include making direct use of hardware primitives for atomic operations (such as interlocked exchange, or compare and swap) or employing regular loads and stores for the purpose of synchronization. Unfortunately, such “low-lock” programs are notoriously difficult to implement systems with a relaxed memory consistency model. Subtle bugs can arise in these programs due to memory operation reordering caused by the relaxed memory model of the underlying hardware. These errors are hard to find and debug as they most often show up only in specific thread interleavings and in particular hardware configurations.
Low-lock code is used heavily both in low-level libraries and in critical paths of a system. Because these parts of the system are crucial to the reliability of the entire system, it is important to develop verification techniques. However, the high degree of non-determinism in relaxed memory consistency models challenges standard verification techniques.
Previous attempts to programmatically find relaxed memory model bugs have attempted to solve the problem by modeling the potential executions of a program executing on a computer having a relaxed memory model. Due to the afore-mentioned non-determinism, these attempts do not scale.
The memory consistency model is one of the major attributes of shared memory multiprocessor systems. It establishes a contract between the hardware and software regarding the behavior of accesses to shared memory. Its implication is not only limited to functionality; it also impacts performance and programmability of the system as well as portability on the software side and compatibility on the hardware side.